event_system{i:l}
== E:Type
==  (eq:EqDecider(E)
==  pred?:(E(?E))
==  info:(E((:Id  Id) + (:(:IdLnk  E)  Id)))
==  oaxioms:EOrderAxioms(E;pred?;info)
==  T:(IdIdType)
==  V:(IdIdType)
==  M:(IdLnkIdType)
==  init:(i:IdEState((T(i))))
==  Trans:(i:Idk:Kndkindcase(k; a.(V(i,a)); l,t.(M(l,t)))EState((T(i)))EState((T(i))))
==  val:(e:Ekindcase(kind(e); a.(V(loc(e),a)); l,t.(M(l,t))))
==  Send:(i:Idk:Kndkindcase(k; a.(V(i,a)); l,t.(M(l,t)))(x:IdT(i,x))(Msg(M) List))
==  Choose:(i,a:Id(x:IdT(i,x))(?(V(i,a))))
==  time:(Erationals)
==  va:val-axiom(E;V;M;info;pred?;
==  va:init;Trans;
==  va:Choose;Send;val;time)
==  opres:(e,e':E. e < e'  qle((time(e)); (time(e'))))
==  discrete:(IdId)
==  (consts:(i,x:Id.
==  (consts:((discrete(i,x)))
==  (consts: (constant_function((init(i,x)); rationals; (T(i,x)))
==  (consts:  (k:Knd, v:kindcase(k; a.(V(i,a)); l,t.(M(l,t))), s:EState((T(i))).
==  (consts:  constant_function((s(x)); rationals; (T(i,x)))
==  (consts:   constant_function((Trans(i,k,v,s,x)); rationals; (T(i,x))))))
==  top)) 

latex

---

clarification:

event_system{i:l}
== E:Type{i}
==  (eq:EqDecider(E)
==  pred?:(E(E + Unit))
==  info:(E((:Id  Id) + (:(:IdLnk  E)  Id)))
==  oaxioms:EOrderAxioms{i:l}
==  oaxioms:EOrderAxioms(E; pred?; info)
==  T:(IdIdType{i})
==  V:(IdIdType{i})
==  M:(IdLnkIdType{i})
==  init:(i:IdEState((T(i))))
==  Trans:(i:Idk:Kndkindcase(k; a.(V(i,a)); l,t.(M(l,t)))EState((T(i)))EState((T(i))))
==  val:(e:Ekindcase(kind(info;e); a.(V(loc(info;e),a)); l,t.(M(l,t))))
==  Send:(i:Idk:Kndkindcase(k; a.(V(i,a)); l,t.(M(l,t)))(x:IdT(i,x))(Msg(M) List))
==  Choose:(i:Ida:Id(x:IdT(i,x))((V(i,a)) + Unit))
==  time:(Erationals)
==  va:val-axiom(E;V;M;info;pred?;
==  va:init;Trans;
==  va:Choose;Send;val;time)
==  opres:(e:E, e':E. cless(E;pred?;info;e;e')  qle((time(e)); (time(e'))))
==  discrete:(IdId)
==  (consts:(i:Id, x:Id.
==  (consts:((discrete(i,x)))
==  (consts: (constant_function((init(i,x)); rationals; (T(i,x)))
==  (consts:  (k:Knd, v:kindcase(k; a.(V(i,a)); l,t.(M(l,t))), s:EState((T(i))).
==  (consts:  constant_function((s(x)); rationals; (T(i,x)))
==  (consts:   constant_function((Trans(i,k,v,s,x)); rationals; (T(i,x))))))
==  top)) 

latex

Definitions	EqDecider(T), EOrderAxioms(E;pred?;info), IdLnk, Type, kind(e), loc(e), type List, Msg(M), , left + right, Unit, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', qle(r; s), x:AB(x), , x:A  B(x), Id, b, P  Q, Knd, kindcase(k; a.f(a); l,t.g(l;t)), x:A. B(x), EState(T), P  Q, constant_function(f; A; B), rationals, f(a), top
FDL editor aliases	ES